انجمنصفحه اولجستجوی انجمن

[لهمشد]

ممکنه این رو بگید چه معنی می کنید؟

کد:

we buit a C front-end in the microsoft visual studio(VS) parallel debuger enviorment through with user can submit short(but trickly)MPI programs, with embedded assertions.

[ف.ش]

(۱۰ اردیبهشت ۱۳۹۰ ۱۲:۲۴ ق.ظ)لهمشد نوشته شده توسط:  ممکنه این رو بگید چه معنی می کنید؟

کد:

we buit a C front-end in the microsoft visual studio(VS) parallel debuger enviorment through with user can submit short(but trickly)MPI programs, with embedded assertions.

ما ساختیم یک سی جلوبندی در محیط دیباگر ویژوال استادیو بواسطه کاربر میتونه ارسال کنه برنامه های‌ام پی آی کوتاه همراه با اعلانهای ذخیره شده .

دوستان لطفا اگه کسی ترجمه بهتر و مفهومی تری داره بگه.ممنون

[لهمشد]

با سلام این رو بررسی کنید لطفا:

کد:

we buit a C front-end in the microsoft visual studio(VS) parallel debugger enviroment through with user can submit short(but tricky) MPI(message passing interface) programs, with embedded assertions .the embedding C statements as well as the MPI (message passing interface)calls are turned into TLA+, run through the TLC model checker.when the assertion fail ,the error traces turn into the vs debugger stepping commands.this approach gives the practitioner a tool for understanding MPI (message passing interface)validated by experts.our formal specification maintains cross-reference tags with MPI reference document ,citing line and page number of pertinent references.another project with similar motivations (but not a C front-end) is,which formalizes the kernel threads procedures of the WIN32 API.

لطفا ترجمه لغت به لغت نکنید مفهوم رو بگید چون من ترجمه نمی خوام مفهوم رو می خوام .

[polarisia]

(۰۹ اردیبهشت ۱۳۹۰ ۰۳:۲۱ ب.ظ)لهمشد نوشته شده توسط:  

کد:

it is well documented that even experienced programmers misunderstand complex libraries such as MPI .Unfortunately,none of the current resource they have to clarify their understanding are satisfactory: the mixture of natural language and semi-formal notations used in standard documents can be misinterpreted,the behavior they observe through "experiments" conducted on actual platform only reveal how someone else has implemented the API ,and formal specifications. as they are written and made available ,are of little direct help to practitioners.with the move to multicores and other novel platforms,API specification emphasize "what" and not "how" may lead to more efficient implementations. program analysis,verification,and platform testing of API implementations all can benefit from formal specifications.

من خودم ترجمه کردم ولی یه جاهایی مفهوم رو نمی فهمم چی می خواد بگه اگه میشه کمک کنید .

واضح است که حتی برنامه نویسان مجرب نیز قادر به درک صحیح و کامل کتابخانه‌های پیچیده‌ای همچون MPI نیستند.
متاسفانه، هیچکدام از منابع کنونی که آنها باید برای درک بهتر از آنها بهره ببرند راضی کننده و مناسب نیستند.
ترکیب زبان طبیعی و نمادهای نیمه رسمی استفاده شده در مستندهای استاندارد میتواند باعث سردرگمی و گمراهی شود.
رفتاری که آنها در طول آزمایشات مربوط به پلتفرمهای واقعی از خود نشان می دهند تنها نشان میدهد که چگونه کسی دیگری API را پیاده سازی کرده است.
مشخصه های رسمی که نوشته و در دسترس قرار میگیرند می تواند کمک اندکی به کارکنان بکند.
با رفتن به سوی پلتفرمهای چند هسته ای و جدید مشخصه‌های API که بر چه چیزی تاکید دارند تا چگونگی می‌توانند باعث پیاده‌سازی‌های کارامدتری شوند.
مشخصه های رسمی می‌تواند برای تحلیل برنامه، اعتبارسنجی. و تست پلتفرم پیاده‌سازی‌های API مفید واقع شود.

[لهمشد]

با سلام این دو قسمت رو می تونید ترجمه کنید:

کد:

bugs in MPI programs arise due to many reasons,for example(i)during manual optimizations that turn blocking send/receives  into their non-blocking counterparts ,(ii) in the context of using wild-card
communications (and the resulting non-determinism),and(iii) in programs that use one-side
  comunication.programmers are acutely aware of the need to test parallel programs  over all their
interleavings.

و این قسمت ؟

کد:

we buit a C front-end in the microsoft visual studio(VS) parallel debugger enviroment through with user can submit short(but tricky) MPI(message passing interface) programs, with embedded assertions .the embedding C statements as well as the MPI (message passing interface)calls are turned into TLA+, run through the TLC model checker.when the assertion fail ,the error traces turn into the vs debugger stepping commands.this approach gives the practitioner a tool for understanding MPI (message passing interface)validated by experts.our formal specification maintains cross-reference tags with MPI reference document ,citing line and page number of pertinent references.another project with similar motivations (but not a C front-end) is,which formalizes the kernel threads procedures of the WIN32 API.

[ف.ش]

[quote='لهمشد' pid='22704' dateline='1304184068']
با سلام این دو قسمت رو می تونید ترجمه کنید:

کد:

bugs in MPI programs arise due to many reasons,for example(i)during manual optimizations that turn blocking send/receives  into their non-blocking counterparts ,(ii) in the context of using wild-card
communications (and the resulting non-determinism),and(iii) in programs that use one-side
  comunication.programmers are acutely aware of the need to test parallel programs  over all their
interleavings.

اشکالات در برنامه های MPI به دلایل مختلف بوجود می آیند برای مثال در طول بهینه سازی های دستی که دریافت/ارسال مسدود را به نقاط مقابل غیرمسدودشان تغییر میدهند در زمینه استفاده از ارتباطات wild-card.( و نتایج غیر اجباری ؟!) و در برنامه هایی که استفاده میکند از ارتباطات یک طرفه.برنامه نویسان بشدت از احتیاج به امتحان برنامه های موازی روی همه ? شان آگاه هستند.

[لهمشد]

سلام به همگی:

معنی این خط چیه؟؟
understanding and accurately modeling them is tedious upfront effort.

[ف.ش]

(۱۲ اردیبهشت ۱۳۹۰ ۱۲:۴۱ ب.ظ)لهمشد نوشته شده توسط:  سلام به همگی:

معنی این خط چیه؟؟
understanding and accurately modeling them is tedious upfront effort.

فهمیدن و مدلسازی دقیق آنها تلاش خسته کننده ای است !؟!!؟!؟!؟!؟!

upfront رو نمیدونم!

[polarisia]

(۱۲ اردیبهشت ۱۳۹۰ ۱۲:۴۶ ب.ظ)afagh1389 نوشته شده توسط:  

(12 اردیبهشت ۱۳۹۰ ۱۲:۴۱ ب.ظ)لهمشد نوشته شده توسط:  سلام به همگی:

معنی این خط چیه؟؟
understanding and accurately modeling them is tedious upfront effort.

فهمیدن و مدلسازی دقیق آنها تلاش خسته کننده ای است !؟!!؟!؟!؟!؟!

upfront رو نمیدونم!

به نظرم اینجا معنی "پیش رو" داره.

"درک و مدلسازی درست و دقیق آنها کاریست خسته کننده که در پیش است."

[لهمشد]

با سلام:
از افاق و polarisa ممنونم(تشکر رسمی)
upfront=رو به جلو - در پیش رو --- معنیش می شد .

کد:

last but not least , it suggests ways to combine static analysis and ISP-BASED model checking.

کد:

this allows the scheduler to march the processes of a given MPI program according to one arbitery interleaving ,till all processes hit MPI_finalize.

همین دوتای اخر

[Fardad-A]

جمله اول:آخرین از حیث ترتیب(یعنی نه کم اهمیت ترین )آن روشهایی را برای ترکیب آنالیز استاتیک(ایستا) و چک کردن مدل ISP-Based پیشنهاد میکند.
جمله دوم:
این به زمانبند اجازه میده تا مطابق یک اینترلیوینگ دلخواه(برگ برگ سازی دلخوا) در پرو سسها (فرایندها)ی یک برنامه MpI داده شده پیشروی کنه تا همه فرآیندها به نقطه انتهای MPi برسند.

[لهمشد]

کد:

this allows the scheduler to march the processes of a given MPI program according to one arbitrary interleaving ,till all processes hit MPI_finalize.ISP examines the resulting trace of actions, and records at each of its choice points, where a different process could have been selected.such alternative choices are deemed necessary based on the dynamic dependence between action in the current trace. if ,at choice point i a different process p' is deemed necessary to have been run ,ISP (which is implemented using "stateless search ") re-executes the entire MPI program till it comes to choiزe point i ,and picks p' to run.

بچه‌ها خدایی خیلی خیلی شرمنده من متوجه نمیشم که این قسمت چی داره میگه لطفا کمک کمک کمک کنید .

[polarisia]

(۱۲ اردیبهشت ۱۳۹۰ ۰۵:۵۱ ب.ظ)لهمشد نوشته شده توسط:  

کد:

this allows the scheduler to march the processes of a given MPI program according to one arbitrary interleaving ,till all processes hit MPI_finalize.ISP examines the resulting trace of actions, and records at each of its choice points, where a different process could have been selected.such alternative choices are deemed necessary based on the dynamic dependence between action in the current trace. if ,at choice point i a different process p' is deemed necessary to have been run ,ISP (which is implemented using "stateless search ") re-executes the entire MPI program till it comes to choiزe point i ,and picks p' to run.

بچه‌ها خدایی خیلی خیلی شرمنده من متوجه نمیشم که این قسمت چی داره میگه لطفا کمک کمک کمک کنید .

اینکار به زمانبند اجازه میدهد تا پروسسهای یک MPI را مطابق با یک interleave( معادل فارسی خوبی نداره: در هم چینی یا همون برگ برگ سازی) تصادفی پیش ببرد تا زمانیکه همه‌ی پروسسها به پایان برسند.
ISP اثرات اعمال و رفتار مورد نتیجه را در حالتیکه پروسس دیگری را در لحظه گزینش، انتخاب میکرد در هر بار از لحظات گزینش بررسی میکند.( یعنی بررسی می کند که اگر پروسس دیگری را (در زمانیکه باید پروسسی را انتخاب کند - لحظه گزینش- )انتخاب میکرد چه میشد.)
انتخابهای جایگزین بر طبق وابستگی پویا بین اعمال در مرحله کنونی، ضروری بنظر میرسند. اگر، در لحظه گزینش i پروسس دیگری مانند p بایستی اجرا میشده، ISP( که با استفاده از "جستجوی بدون حالت" پیاده سازی شده است )دوباره تمام برنامه MPI را اجرا می کند تا به نقطه‌ی i برسد و اینبار پروسس p را برای اجرا انتخاب می‌کند.

[لهمشد]

با سلام:
ممکنه این رو بررسی کنید.

کد:

for model checking to be successful in practice :(I) designer must have modestly expensive techniques to create models of the protocols to be verified.(I)they must be able to examine a fraction of the interleaving in  concurrent system and be able to claim that the remaining interleaving are equivalent and hence need not be examined ,using a suitable partial order reduction algorithm

[**sara**]

(۱۲ اردیبهشت ۱۳۹۰ ۰۶:۳۲ ب.ظ)polarisia نوشته شده توسط:  

کد:

this allows the scheduler to march the processes of a given MPI program according to one arbitrary interleaving ,till all processes hit MPI_finalize.

اینکار به زمانبند اجازه میدهد تا پروسسهای یک MPI را مطابق با یک interleave( معادل فارسی خوبی نداره: در هم چینی یا همون برگ برگ سازی) تصادفی پیش ببرد تا زمانیکه همه‌ی پروسسها به پایان برسند.

برای معادل فارسی interleave کلمه "جایگذاری" خوبه؟

---

کد:

for model checking to be successful in practice :(I) designer must have modestly expensive techniques to create models of the protocols to be verified.(I)they must be able to examine a fraction of the interleaving in  concurrent system and be able to claim that the remaining interleaving are equivalent and hence need not be examined ,using a suitable partial order reduction algorithm

برای موفقیت بررسی مدل در عمل:
(I) طراح باید تکنیک های نسبتاً گران قیمتی داشته باشد، تا مدل پروتکل هایی را بسازد که تائید شوند. (II) آنها باید قادر به بررسی بخشی از جایگذاری در سیستم همزمان باشند و بتوانند ادعا کنند که با اثر باقیمانده از جایگذاری معادلند و از این رو با استفاده از یک الگوریتم مناسب جهت کاهش جزئی، نیازی به بررسی ندارند.